|
A subsumption lattice is a mathematical structure used in theoretical background of automated theorem proving and other symbolic computation applications. ==Definition== A term ''t''1 is said to ''subsume'' a term ''t''2 if a substitution ''σ'' exists such that ''σ'' applied to ''t''1 yields ''t''2. In this case, ''t''1 is also called ''more general than'' ''t''2, and ''t''2 is called ''more specific than'' ''t''1, or ''an instance of'' ''t''1. The set of all (first-order) terms over a given signature can be made a lattice over the partial ordering relation "''... is more specific than ...''" as follows: * consider two terms equal if they differ only in their variable naming,〔formally: factorize the set of all terms by the equivalence relation "''... is a renaming of ...''"; for example, the term ''f''(''x'',''y'') is a renaming of ''f''(''y'',''x''), but not of ''f''(''x'',''x'')〕 * add an artificial minimal element Ω (the ''overspecified term''), which is considered to be more specific than any other term. This lattice is called the subsumption lattice. Two terms are said to be unifiable if their meet differs from Ω. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Subsumption lattice」の詳細全文を読む スポンサード リンク
|